$\forall$${\it da}$:fpf(Knd; $k$.Type), $l$:IdLnk, ${\it tg}$:Id, $T$:top. \\[0ex]sqequal(fpf{-}cap(es{-}dt($l$; ${\it da}$); id{-}deq; ${\it tg}$; $T$); fpf{-}cap(${\it da}$; Kind{-}deq; rcv($l$,${\it tg}$); $T$))